$\forall$$A$, $B$:Type, $L$:(($A$$\rightarrow$($B$ + Top)) List), $x$:$A$.
\\[0ex]($\uparrow$can{-}apply(p{-}first($L$);$x$))
\\[0ex]$\Rightarrow$ (do{-}apply(p{-}first($L$);$x$) = do{-}apply(hd(filter($\lambda$$f$.can{-}apply($f$;$x$);$L$));$x$) $\in$ $B$)